Quality assurance of computer programs may be desired. However, validating computer programs may be a hard task because the computer program represents a system may have a significant number of potential states and potentially infinite number of states, making the verification problem undecidable.
Coverage analysis provides metrics that attempt to indicate thoroughness of validation. In testing, there exist numerous coverage metrics that serve as heuristic measures of exhaustiveness of a test suite. In formal verification of software, no such metrics exist. The straightforward metrics that check line and branch coverage are not very useful in formal verification, since taking a branch or looking at a line does not necessarily means that it was exhaustively analyzed.
Computer programs may comprise a loop which may be performed iteratively. Such loops may potentially be unbounded and may be performed forever. Such as scenario is exhibited, for example, in a reactive system, in which an unbounded loop is performed until an event is detected and corresponding actions, which may or may not be deterministic, are performed. After performing those actions, the system may perform the loop once more to detect an event and potentially react to the event.
Formal verification is a technique in which the computerized component is modeled and is examined by a model checker. A verification query comprises a model and a property, wherein the model is to be checked whether it holds the property or there exists a behavior of the model that refutes the property. The model describes all possible functional behaviors of the computerized component based on inputs from the environment and calculations performed by the computerized component itself. Most components are represented by cycled models in which the state of the component may differ from one cycle to the other. It will be noted that the computerized component may be a software component, firmware component, hardware component or the like.
In software formal verification, the model may be deemed as changing a cycle upon modification to the program counter or program instructor. Alternatively, other temporal schemas may be used.
A model checker checks that the model holds a predetermined specification property. An exemplary specification property may be that a triggered event is always handled by the component or that a certain variable is never assigned a predetermined value. The specification property may be attributed to one or more cycles, such as for example, after a flag is raised in a cycle, an alert is eventually issued. In some exemplary embodiments, the property may be any property such as safety property or liveness property, and may be provided using a Property Specification Language (PSL) formula such as AGp, indicating that Always (i.e., in each cycle), Globally (i.e. in each possible scenario), property p holds. Property p may be a property provided in temporal logic.
Model checkers may be symbolic model checkers, explicit model checkers, or the like. The model checker may utilize a Boolean Satisfiability problem (SAT) solver, and known as SAT-based model checkers, such as for example a Bounded Model Checker (BMC), Interpolant-based Transition Relation approximation, or the like. Additionally or alternatively, model checkers may be Binary Decision Diagrams (BDD)-based model checker.
ExpliSAT™ is a hybrid formal verification for software model checking that combines explicit-state and symbolic techniques, wherein the control flow graph of the program is explicitly traversed. ExpliSAT is disclosed in S. Barner, C. Eisner, Z. Glazberg, D. Kroening, I. Rabinovitz, “ExpliSAT: Guiding SAT-Based Software Verification with Explicit States”, HVC 2006, which is hereby incorporated by reference in its entirety.